Step of Proof: append_overlapping_sublists 11,40
Inference at * 1 2 1 0 
Iof proof for Lemma append overlapping sublists:

.....wf..... NILNIL

1. T : Type
2. L1 : T List
3. L2 : T List
4. L : T List
5. x : T
6. i, j:. (i < ||L||)  (j < ||L||)  ((i = j))  ((L[i] = L[j]))
7. f1 : {0..||L1 @ [x]||}{0..||L||}
8. increasing(f1;||L1 @ [x]||)
9. j:{0..||L1 @ [x]||}. (L1 @ [x])[j] = L[(f1(j))]
10. f : {0..(||L2||+1)}{0..||L||}
11. increasing(f;||L2||+1)
12. j:{0..(||L2||+1)}. [x / L2][j] = L[(f(j))]
13. ||L1 @ [x / L2]|| = ||L1||+||L2||+1
14. ||[]||  0 
  (i.if i z ||L1|| then f1(i) else f(i - ||L1||) fi )
   {0..||L1 @ [x / L2]||}{0..||L||} 
latex
 by PERMUTE{1:n,
 by PERMUTE{2:n,
 by PERMUTE{3:n,
 by PERMUTE{4:n,
 by PERMUTE{5:n,
 by PERMUTE{6:n,
 by PERMUTE{7:n,
 by PERMUTE{8:n,
 by PERMUTE{9:n,
 by PERMUTE{10:n,
 by PERMUTE{11:n,
 by PERMUTE{12:n,
 by PERMUTE{10:n,
 by PERMUTE{13:n,
 by PERMUTE{11:n,
 by PERMUTE{14:n,
 by PERMUTE{15:n,
 by PERMUTE{16:n,
 by PERMUTE{17:n,
 by PERMUTE{18:n,
 by PERMUTE{16:n,
 by PERMUTE{15:n,
 by PERMUTE{19:n} 
latex

 1: .....wf..... NILNIL

 1: 15. i : {0..||L1 @ [x / L2]||}
 1:   i z ||L1||  
 2: .....wf..... NILNIL

 2: 15. {0..||L1 @ [x / L2]||}
 2:     Type
 3: .....wf..... NILNIL

 3: 15. i : {0..||L1 @ [x / L2]||}
 3: 16. i z ||L1|| = tt
 3:   (i z ||L1|| = tt)  
 4: .....wf..... NILNIL

 4: 15. i : {0..||L1 @ [x / L2]||}
 4: 16. i z ||L1|| = tt
 4:   (i z ||L1||)  
 5: .....wf..... NILNIL

 5: 15. i : {0..||L1 @ [x / L2]||}
 5: 16. i z ||L1|| = tt
 5:   (i  ||L1||)  
 6: .....wf..... NILNIL

 6: 15. i : {0..||L1 @ [x / L2]||}
 6: 16. i z ||L1|| = tt
 6:   i z ||L1||  
 7: .....wf..... NILNIL

 7: 15. i : {0..||L1 @ [x / L2]||}
 7: 16. i z ||L1|| = tt
 7:   i  
 8: .....wf..... NILNIL

 8: 15. i : {0..||L1 @ [x / L2]||}
 8: 16. i z ||L1|| = tt
 8:   ||L1||  
 9: .....truecase..... NILNIL

 9: 15. i : {0..||L1 @ [x / L2]||}
 9: 16. i  ||L1||
 9:   f1(i)  {0..||L||}
 10: .....wf..... NILNIL

 10: 15. i : {0..||L1 @ [x / L2]||}
 10: 16. i z ||L1|| = ff
 10:   (i z ||L1|| = ff)  
 11: .....wf..... NILNIL

 11: 15. i : {0..||L1 @ [x / L2]||}
 11: 16. i z ||L1|| = ff
 11:   (||L1|| <z i)  
 12: .....wf..... NILNIL

 12: 15. i : {0..||L1 @ [x / L2]||}
 12: 16. i z ||L1|| = ff
 12:   (||L1|| < i)  
 13: .....wf..... NILNIL

 13: 15. i : {0..||L1 @ [x / L2]||}
 13: 16. i z ||L1|| = ff
 13:   ((i z ||L1||))  
 14: .....wf..... NILNIL

 14: 15. i : {0..||L1 @ [x / L2]||}
 14: 16. i z ||L1|| = ff
 14:   i z ||L1||  
 15: .....wf..... NILNIL

 15: 15. i : {0..||L1 @ [x / L2]||}
 15: 16. i z ||L1|| = ff
 15:   i  
 16: .....wf..... NILNIL

 16: 15. i : {0..||L1 @ [x / L2]||}
 16: 16. i z ||L1|| = ff
 16:   ||L1||  
 17: .....antecedent..... NILNIL

 17: 15. i : {0..||L1 @ [x / L2]||}
 17: 16. i z ||L1|| = ff
 17:   True
 18: .....wf..... NILNIL

 18: 15. i : {0..||L1 @ [x / L2]||}
 18: 16. i z ||L1|| = ff
 18: 17. ((i z ||L1||)) = (||L1|| <z i)
 18:    = 
 19: .....falsecase..... NILNIL

 19: 15. i : {0..||L1 @ [x / L2]||}
 19: 16. ||L1|| < i
 19:   f(i - ||L1||)  {0..||L||}
 .

Definitions{x:A| B(x)} , b, i <z j, inr x , case b of inl(x) => s(x) | inr(y) => t(y), x:A  B(x), b, A  B, , Ax, inl x , left + right, n - m, i z j, x.A(x), i  j , , n+m, f(a), increasing(f;k), [], [car / cdr], as @ bs, #$n, {i..j}, x:AB(x), l[i], s = t, A, ||as||, a < b, , type List, Type, , Unit, , True, T, ff, P  Q, P & Q, P  Q, tt, if b then t else f fi , t  T, P  Q, x:A. B(x)
Lemmasint seg wf, assert of lt int, bnot of le int, bool wf, true wf, squash wf, assert wf, eqff to assert, assert of le int, eqtt to assert, iff transitivity

origin